l:IdLnk, dt:fpf(Id; tg.Type), knd:Knd, T:Type.
((isrcv(knd))
 (eq_lnk(lnk(knd); l))
 (fpf-dom(id-deq; tag(knd); dt))
 (T = fpf-ap(dt; id-deq; tag(knd))))
 fpf-compatible(Knd; x.Type; Kind-deq; lnk-decl(l; dt); fpf-single(knd; T)) 

latex

Definitions

Knd, Type, lnk-decl(l; dt), fpf-ap(f; eq; x), <a, b>, s = t, P  Q, t  T, guard(T), x:A. B(x), sq_type(T), prop{i:l}, sqequal(s; t), left + right, void, isect(A; x.B(x)), top, Kind-deq, x:AB(x), x:A  B(x), P  Q, P  Q, x. t(x), fpf(A; a.B(a)), x.A(x), fpf-single(x; v), fpf-dom(eq; x; f), b, fpf-compatible(A; a.B(a); eq; f; g), IdLnk, Id, tag(k), id-deq, lnk(k), eq_lnk(a; b), isrcv(k), rcv(l,tg), t.1, map(f; as), type List, x:A. B(x), True, P  Q, decidable(P), False, P  Q, A

Lemmas

assert-eq-lnk, decidable assert, member map, map wf, rcv wf, assert-deq-member, isrcv wf, eq lnk wf, lnk wf, fpf-ap wf, id-deq wf, tagof wf, Id wf, IdLnk wf, assert wf, fpf-dom wf, fpf-single wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, top wf, fpf-single-dom, Kind-deq wf, Knd wf, Knd sq